A. Avron; 1984; "On Modal Systems Having Arithmetical Interpretations"

著者

メモ

飽和(saturated)シーケントというものを考えて，Kripkeモデルの状態$ Wとしてシーケントの集まりを考えるという手法が面白かった．

が，証明が何か間違っている気がしたため途中で読むのをやめている．

Kripke意味論の与え方が違う可能性はある．

少なくとも付値関数$ V \colon \mathrm{Prop} \to 2^Wではなく$ V \colon W \times \mathrm{Prop} \to 2となっている（実際には拡張されて$ V' \colon W \times \mathrm{Fml} \to 2）

様相論理S4Grzの話もあるが，このメモでは省略している．

Def: 飽和シークエント

シーケント$ \Gamma \rArr \Deltaが飽和(saturated)しているとは，

任意の$ A \oplus Bの形をした論理式（ただし$ \oplus \equiv \land, \lor, \to）に対し，

1. $ A \oplus B \in \Delta \implies A \in \Gamma ~\&~ B \in \Delta

2. $ A \oplus B \in \Gamma \implies B \in \Gamma ~\&~ A \in \Delta

を満たしていることとする．

Prop 1

$ \Gamma \rArr \Deltaが$ \sf GLカット無し証明可能なら，

$ \Gamma \sube \Gamma', \Delta \sube \Delta'かつ，$ \Gamma \rArr \Delta'もカット無し証明可能となる飽和シーケント$ \Gamma' \rArr \Delta'が存在する．

この$ \Gamma'\rArr\Delta'を$ \Gamma \rArr \Deltaの飽和シーケントという．

Def: 証明可能性論理GLのシークエント計算体系$ \mathfrak{S}_\mathsf{GL}

D. Leviant; 1981; "On the proof theory of the modal logic for arithmetic provability"に基づき，$ (\Box_\mathsf{GL})規則$ \dfrac{\Box A, \Box\Gamma, \Gamma \rArr A}{\Box\Gamma \rArr \Box A}を追加した体系とする．

Thm 2

次を満たすKripkeモデル$ \mathcal{M} = \lang D, \prec, V \rangが存在する．

1. $ \precは推移的かつ非反射的

2. 任意の$ d \in Dに対し，$ \{d' \mid d' \prec d\}は有限．

すなわち，Kripkeフレーム$ \lang D, \prec \rangは整礎関係である．

3. $ \Gamma \rArr \Deltaが$ \mathfrak{S}_\mathsf{GL}でカット無しで証明可能なら，ある$ d \in Dが存在し，

$ \gamma \in \Gammaに対し$ V(d, \gamma) = \mathrm{T}

$ \delta \in \Deltaに対し$ V(d, \delta) = \mathrm{F}

Thm2から以下の系が得られる

memo

論文にはこれらの結論をどうやって得るかの証明が書いていない．

Cor 2.1: 証明可能性論理GLのカット除去定理 / 意味論的カット除去定理

$ \mathfrak{S}_\mathsf{GL}ではカット除去定理が成り立つ．

ref:

G. Sambin, S. Valentini; 1980; "The Modal Logic of Provability. The Sequential Approach"

構文論的カット除去定理はD. Leviant; 1981; "On the proof theory of the modal logic for arithmetic provability"に書かれているが，ミスがあるらしい．

Cor 2.2: 証明可能性論理GLは有限フレーム性がある

$ \sf GLは推移的かつ整礎な有限フレームに対して完全

Cor 2.3: Solovayの算術的完全性定理の言い換え？

命題変項$ p_1,\dots,p_nを含んだ$ \sf GLの論理式$ A(p_1,\dots,p_n)が$ \sf GLで証明不能なら，$ \sf PAの拡大理論$ Tへの解釈(証明可能性論理)$ f_Tを用意して$ f(p_i) \mapsto \sigma_iとしたとき（$ \sigma_iは算術の文），$ \nvdash_\mathsf{PA} f_T(A(p_1,\dots,p_n))

remark:

Robert M. Solovay; 1976; "Provability Interpretation of Modal Logic"の構成法と書かれているが，多分現代的な視座なら解釈(証明可能性論理)のことだと思う．

Cor 2.4:

$ p_i,q_i \equiv p, \botとする．

シーケント$ p_1,\dots,p_k, \Box\varphi_1,\dots,\Box\varphi_n \rArr q_1,\dots,q_l, \Box\psi_1,\dots,\Box\psi_mは以下の条件のうちどれかを満たせば証明可能．

a. ある$ i,jで$ p_i \equiv q_j

b. $ p_i \equiv \bot

c. $ m \neq 0かつ$ 1 \leq j \leq mなある$ jで$ \vdash_{\mathfrak{S}_\mathsf{GL}} \Box \psi_j, \Box\varphi_1,\varphi_1,\dots,\Box\varphi_n,\varphi_n \rArr \psi_j

memo

This corollary can be used for an easy and practical decision procedure.

Proof of Thm.2

次のKripkeモデル$ \mathcal{M} = \lang D, \prec, V \rangを考える．

全ての$ \sf GLカット無し証明可能な飽和シーケントの集合を$ Dとする

$ \Gamma_1 \rArr \Delta_1 \prec \Gamma_2 \rArr \Delta_2とは以下のように定義する．　

a. $ \varphi \in \Gamma_1 \cup \Delta_1 \implies \varphi \in \mathrm{Sub}(\Gamma_2 \rArr \Delta_2)

b. $ \Box \varphi \in \Gamma_2 \implies \varphi, \Box\varphi \in \Gamma_1

c. $ \Box \varphi \in \Gamma_1 ~\&~ \Box\varphi \notin \Gamma_2な$ \Box\varphiが存在する．

$ p \in \mathrm{Prop}として，$ V(\Gamma \rArr \Delta, p) = \mathrm{T} \iff p \in \Gamma

このモデルは条件1,2を満たすことがわかる．

memo:そんなに自明ではない．

条件3を満たすかチェックする．論理式の複雑さの帰納法によって以下を示す

i. $ A \in \Gamma \implies V(\Gamma \rArr \Delta, A) = \mathrm{T}

ii. $ A \in \Delta \implies V(\Gamma \rArr \Delta, A) = \mathrm{F}

$ A \equiv p,\botなら自明．

$ A \equiv B \to Cの場合は

i. $ B \to C \in \Gamma

飽和シーケントの定義より$ \implies$ C \in \Gamma ~\&~ B \in \Delta

帰納法の仮定より$ V(\Gamma \rArr \Delta, C) = \mathrm{T} ~\&~ V(\Gamma \rArr \Delta, B) = \mathrm{F}

Kripkeモデルの意味論より$ V(\Gamma \rArr \Delta, B \to C) = \mathrm{T}

iiも同様にやればよい．

$ A \equiv B \land C, B \lor Cなども同様．

$ A \equiv \Box Bとする．

i. $ \Box B \in \Gammaなら

$ \precの定義bより$ \Gamma' \rArr \Delta' \prec \Gamma \rArr \Deltaとなる任意の$ \Gamma' \rArr \Delta'について$ B \in \Gamma'

IHより$ V(\Gamma' \rArr \Delta', B) = \mathrm{T}であるので$ V(\Gamma' \rArr \Delta', \Box B) = \mathrm{T}

したがって$ V(\Gamma \rArr \Delta, \Box B) = \mathrm{T}

SnO2WMaN.iconとなっているが，どう考えてもここ間違ってるんじゃないかと思う．

$ \precの向きが逆じゃないか？

ii. $ \Box B \in \Delta

$ \Gammaに含まれる$ \Box \gammaの形の全ての論理式$ \Box\gamma_1,\dots,\Box\gamma_n \in \Gammaとする．

$ \Box B, \Box\gamma_1,\gamma_1,\dots,\Box\gamma_n,\gamma_n \rArr Bは$ \sf GLカット無し証明可能．

$ \Gamma \rArr \Deltaは$ \sf GLカット無し証明可能なので$ (\Box_\mathsf{GL})規則や弱化などで

このシーケントの飽和シーケント$ \Gamma' \rArr \Delta'を取れば自明に$ \Gamma' \rArr \Delta' \prec \Gamma \rArr \Delta

IHより$ V(\Gamma' \rArr \Delta', B) = \mathrm{F}

したがって$ V(\Gamma \rArr \Delta, \Box B) = \mathrm{F}

SnO2WMaN.icon↑同様にここも間違っている気がする．

以上よりこのKripkeモデルは定理の要請を満たす．❏